L:Knd List, l:IdLnk, tg:Id.
@source(l): only L sends on (l with tg)  Dsys
& (D:Dsys.
& (@source(l): only L sends on (l with tg)  D
& ( D 
& ( realizes es.
& ( e:E.
& ( loc(e) = destination(l)  Id  kind(e) = rcv(l,tg)  Knd  (kind(sender(e))  L)) 

latex

Definitions

x:A. B(x), A & B, t  T, P  Q, D realizes es. P(es), Prop, S  T, A, sends(l,tg,e), P & Q, SQType(T), {T}, lnk(e), rcv(l,tg), lnk(k), 1of(t), outl(x), (x  l), x:A. B(x), , msg(l;t;v), tag(e), mtag(m), mtag(m), tag(k), 2of(t), P  Q, P  Q, (Msg on l), {i..j}, ||as||, Y

Lemmas

s-sframe-rule, lsrc wf, es-sender wf, es-kind-rcv, Knd wf, es-kind wf, w-es wf, rcv wf, es-loc wf, ldst wf, es-E wf, possible-world wf, fair-fifo wf, world wf, d-sub wf, dsys wf, Id wf, IdLnk wf, not functionality wrt iff, assert wf, null wf3, es-tg-sends wf, assert of null, es-axioms, member filter, es-Msg wf, eq id wf, es-mtag wf, es-sends wf, IdLnk sq, es-lnk wf, Knd sq, es-index wf, int seg wf, length wf1, es-Msgl wf, select wf, assert-eq-id, l member wf